package com.googlecode.kipler.satisfiability.clash;

import java.util.HashSet;
import java.util.Set;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.DependencyManager;
import com.googlecode.kipler.container.dl.DependencySet;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.rule.trace.RuleTrace;
import com.googlecode.kipler.satisfiability.completion.rule.trace.RuleType;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class BasicClashDetectionStrategy implements ClashDetectionStrategy {

	private String explanation;

	private DependencySet dependencySet = new DependencySet();

	private Set<Formula> clashCause = new HashSet<Formula>();

	public DependencySet getDependencySet() {
		return dependencySet;
	}

	public boolean hasClash(ABox abox, Formula formula) {
		boolean hasClash = false;
		if (formula instanceof ConceptAssertion) {
			ConceptAssertion ca = (ConceptAssertion) formula;
			ConceptAssertion negCa;
			negCa = (ConceptAssertion) ca.copy().toggleNegated();
			hasClash = abox.contains(negCa);
			if (hasClash) {
				dependencySet.clear();
				WorldConstraintSystem wcs = abox.getWorld().getWcs();
				DependencyManager depMan = wcs.getData().getDependencyManager();
				dependencySet.addAll(depMan.getDependencies(ca));
				dependencySet.addAll(depMan.getDependencies(negCa));
				clashCause.add(ca);
				clashCause.add(negCa);
				explanation = ca + " and its negation";
				if (wcs.getReasoner().getProfile().isInterpolationEnabled()) {
					RuleTrace trace = new RuleTrace();
					trace.setType(RuleType.CLASH);
					trace.getConstraints().add(negCa);
					trace.getConstraints().add(ca);
					BasicWcsInterpolationData data = (BasicWcsInterpolationData) wcs
							.getData();
					data.getRuleTracing().add(trace);
				}
			}
		}
		return hasClash;
	}

	public Set<Formula> getClashCause() {
		return clashCause;
	}

	public String getExplanation() {
		return explanation;
	}

}
